$\forall$$M$:MsgA, $k$:Knd, $s$:$M$.state, $v$:$M$.da($k$), $x$:Id. ma{-}ef{-}const($M$;$k$;$x$;$s$;$v$) $\in$ $\mathbb{P}$